$\forall$$A$, $B$:Type, $f$:($A$$\rightarrow$$B$), $g$:($B$$\rightarrow$$A$). InvFuns($A$;$B$;$f$;$g$) $\Rightarrow$ Bij($A$;$B$;$f$)